Nuprl Lemma : exists_functionality_wrt_implies
12,41
postcript
pdf
S
,
T
:Type,
P
,
Q
:(
S
). (
S
=
T
)
(
x
:
S
. {
P
(
x
)
Q
(
x
)})
{(
x
:
S
.
P
(
x
))
(
y
:
T
.
Q
(
y
))}
latex
ProofTree
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
x
(
s
)
,
{
T
}
,
P
Q
,
,
x
:
A
.
B
(
x
)
origin
S, T:Type, P, Q:(S
). (S = T) 
(x:S. {P(x) Q(x)}) {(
x:S. P(x)) (y:T. Q(y))}
S, T:Type, P, Q:(S). (S = T) (x:S. {P(x) Q(x)}) {(x:S. P(x)) (y:T. Q(y))}
Tx:A. B(x) Qx:A. B(x)